greatcfandomcom-20200214-history
Register Machines
Why Study Register Machines? Proof is the silicon substrate for software. Proof should dictate software design and not be post-facto. Two Instruction Language We start with a very simple computer and see how much we can prove about program correctness for programs written in a minimalistic langauge. We will work towards proofs of programs for the OISC computers described in (Gilreath, Laplante, 2003) and computers based on (Mueller, Paul, 1998). The register machine we are going to start with is based on the ideas in (Johnstone, 1987). Such a register machine is normally used to answer questions about computability but we will be using it as a very basic computer to see how far we can get proving programs correct and what problems we encounter on the way. The language/computer that we will start with can be defined as follows: ::= | ::= INC | BNZ Semantics / Transition Rules For the semantics we create a model of a state that consists of a pair, a program counter and a mapping from register names to values. S \equiv (PC, M) Operational Semantics The operational semantics can be summarised as follows: \Delta(INC \; R) \; S = \gets PC + 1, R \gets R + 1 \; S \leq (\Delta INC) \Delta (BNZ \; R \; I) \; S \equiv \gets PC + 1 \; S , M® = 0 \leq (\Delta BNZ_0) \Delta (BNZ \; R \; I) \; S \equiv \gets I, R \gets R - 1 \; S , M® > 0 \leq (\Delta BNZ_1) The following is incorrect. Things are not this simple. \Delta (P1 \; P2) \; S \equiv \Delta (P2) \circ \Delta (P1) \; S \leq (\Delta SEQ) Programs for the Register Machine A program is a sequence of instructions: 0: STOP 1: BNZ R0 1 2: INC RO 3: BNZ R0 0 Execution of a Program A program is executed by: * Setting the initial values of the registers * Setting the initial value of the program counter * Stepping through the program in the context of the registers and program counter During the execution of a program the machine moves from state to state. A state during execution is represented by the value of the program counter and the current value of the registers determined by M. PC = 2 M(R0) = 3 0: STOP 1: BNZ R0 1 2: INC RO 3: BNZ R0 0 Program 1: CLEAR R0 We start with a program that will clear the contents of register R0 leaving it with the value 0 when the program terminates. Let P \equiv PC = 1 M(R0) = N 0: STOP 1: BNZ R0 1 2: INC RO 3: BNZ R0 0 We want to prove \{ S_\bullet = ( 1, M_\bullet ) \} \; P \; \{ S_\odot = ( 0, M_\odot ) where M_\odot ( R_0 ) = 0 \} . Structure 0: STOP <-----+ +---------------------+ | +--> 1: BNZ R0 1 ---+ | 2: INC RO | 3: BNZ R0 0 ------+ Proof We use a proof by induction. Basis of the Induction Show this is true for S_0 = (1, M_0) \; where \; M_0(R_0) = 0 Initial State: 0: STOP S_0 = (1, M_0) \land M_0(R_0) = 0 1: CLEAR BNZ R0 CLEAR 2: INC RO 3: BNZ R0 STOP Apply ΔBNZ0:''' 0: STOP 1: CLEAR BNZ R0 CLEAR S_1 = (2, M_0) 2: INC RO 3: BNZ R0 STOP Apply: ''ΔINC:' 0: STOP 1: CLEAR BNZ R0 CLEAR 2: INC RO S_2 = (3, \gets R_0 + 1 M_0) 3: BNZ R0 STOP Apply ΔBNZ1:''' S_3 = (0, \gets R_0 - 1\gets R_0 + 1 M_0) 0: STOP 1: CLEAR BNZ R0 CLEAR 2: INC RO 3: BNZ R0 STOP Final State Inductive Step Assume that for S_\bullet = (1, M_\bullet) where M_\bullet(R_0) = n we have \{ S_\bullet \} \; P \; \{ S_\odot \} where S_\odot = (0, M_\odot) and M_\odot(R_0) = 0 Initial State 0: STOP S_0 = ( 1, M_0 ) and M_0 ( R_0 ) = n + 1 1: CLEAR BNZ R0 CLEAR 2: INC RO 3: BNZ R0 STOP Apply ''ΔBNZ1:' 0: STOP S_0 = ( 1, M_0 ) and M_0 ( R_0 ) = n which is S_\bullet = (1, M_\bullet) 1: CLEAR BNZ R0 CLEAR 2: INC RO 3: BNZ R0 STOP Final State Hence \{ S_\bullet = ( 1, M_\bullet ) \} \; P \; \{ S_\odot = ( 0, M_\odot ) where M_\odot ( R_0 ) = 0 \} Program 2: JMP I JMP I \equiv PC: INC RX PC+1: BNZ RX I Prove: \{S_\bullet = (PC, M_\bullet)\} \; JMP \; I \; \{S_\odot = (I, M_\bullet\} Proof \{S_\bullet = (PC, M_\bullet)\} Initial state: S_0 = (PC, M_0) PC: INC RX PC+1: BNZ RX I Apply: ΔINC:''' PC: INC RX S_1 = (PC, \gets RX + 1 M_0) PC+1: BNZ RX I Apply ''ΔBNZ1:' PC: INC RX PC+1: BNZ RX I S_2 = (I, \gets RX - 1\gets RX + 1 M_0) = (I, M_0) Final state: \{S_\odot = (I, M_\bullet)\} Category:Research